(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
 Patrice Godefroid, SAGE (systematic dynamic test generation)
 For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun T1_11011 () (_ BitVec 8))
(declare-fun T1_11012 () (_ BitVec 8))
(declare-fun T1_11013 () (_ BitVec 8))
(declare-fun T1_11014 () (_ BitVec 8))
(declare-fun T1_11015 () (_ BitVec 8))
(declare-fun T1_11016 () (_ BitVec 8))
(declare-fun T1_11017 () (_ BitVec 8))
(declare-fun T1_11018 () (_ BitVec 8))
(declare-fun T1_11019 () (_ BitVec 8))
(declare-fun T1_11020 () (_ BitVec 8))
(declare-fun T1_11021 () (_ BitVec 8))
(declare-fun T1_11022 () (_ BitVec 8))
(declare-fun T1_11023 () (_ BitVec 8))
(declare-fun T1_11024 () (_ BitVec 8))
(declare-fun T1_11025 () (_ BitVec 8))
(declare-fun T1_11026 () (_ BitVec 8))
(declare-fun T1_11027 () (_ BitVec 8))
(assert (let ((?v_20 ((_ zero_extend 24) (_ bv1 8))) (?v_2 ((_ zero_extend 24) (_ bv101 8))) (?v_0 (bvand ((_ zero_extend 24) T1_11011) (_ bv223 32)))) (let ((?v_1 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11012) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_0)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_0)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_0)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_0 ?v_2)))) (let ((?v_3 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11013) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_1)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_1)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_1)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_1 ?v_2))) (?v_18 ((_ zero_extend 24) T1_11014))) (let ((?v_4 (bvadd (bvand (bvadd (bvadd (bvadd ?v_18 (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_3)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_3)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_3)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_3 ?v_2)))) (let ((?v_5 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11015) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_4)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_4)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_4)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_4 ?v_2)))) (let ((?v_6 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11016) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_5)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_5)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_5)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_5 ?v_2)))) (let ((?v_7 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11017) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_6)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_6)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_6)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_6 ?v_2)))) (let ((?v_8 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11018) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_7)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_7)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_7)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_7 ?v_2))) (?v_24 ((_ zero_extend 24) T1_11019))) (let ((?v_9 (bvadd (bvand (bvadd (bvadd (bvadd ?v_24 (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_8)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_8)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_8)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_8 ?v_2)))) (let ((?v_10 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11020) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_9)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_9)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_9)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_9 ?v_2)))) (let ((?v_11 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11021) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_10)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_10)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_10)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_10 ?v_2)))) (let ((?v_12 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11022) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_11)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_11)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_11)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_11 ?v_2)))) (let ((?v_13 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11023) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_12)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_12)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_12)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_12 ?v_2))) (?v_68 ((_ zero_extend 24) T1_11024))) (let ((?v_14 (bvadd (bvand (bvadd (bvadd (bvadd ?v_68 (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_13)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_13)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_13)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_13 ?v_2)))) (let ((?v_15 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11025) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_14)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_14)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_14)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_14 ?v_2)))) (let ((?v_16 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11026) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_15)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_15)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_15)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_15 ?v_2)))) (let ((?v_17 (bvadd (bvand (bvadd (bvadd (bvadd ((_ zero_extend 24) T1_11027) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_16)) (_ bv8 32))) (bvshl ((_ zero_extend 24) ((_ extract 23 16) ?v_16)) (_ bv16 32))) (bvshl ((_ zero_extend 24) ((_ extract 31 24) ?v_16)) (_ bv24 32))) (_ bv223 32)) (bvmul ?v_16 ?v_2))) (?v_41 ((_ zero_extend 24) (_ bv16 8)))) (let ((?v_69 (bvor (bvashr (bvadd (bvmul ?v_17 (_ bv1103515245 32)) (_ bv12345 32)) ?v_41) (bvand (bvadd (bvmul ?v_17 (_ bv69069 32)) ?v_20) (_ bv4294901760 32))))) (let ((?v_71 (bvand ?v_69 (_ bv7 32))) (?v_70 ((_ zero_extend 24) (_ bv6 8))) (?v_26 ((_ sign_extend 8) T1_11027)) (?v_28 ((_ sign_extend 8) T1_11025)) (?v_29 ((_ sign_extend 8) T1_11024)) (?v_40 ((_ sign_extend 8) T1_11011))) (let ((?v_65 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_40)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_40)) (_ bv8 32))) (_ bv65503 32))) (?v_39 ((_ sign_extend 8) T1_11012))) (let ((?v_64 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_39)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_39)) (_ bv8 32))) (_ bv65503 32))) (?v_38 ((_ sign_extend 8) T1_11013))) (let ((?v_63 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_38)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_38)) (_ bv8 32))) (_ bv65503 32))) (?v_37 ((_ sign_extend 8) T1_11014))) (let ((?v_62 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_37)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_37)) (_ bv8 32))) (_ bv65503 32))) (?v_36 ((_ sign_extend 8) T1_11015))) (let ((?v_61 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_36)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_36)) (_ bv8 32))) (_ bv65503 32))) (?v_35 ((_ sign_extend 8) T1_11016))) (let ((?v_60 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_35)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_35)) (_ bv8 32))) (_ bv65503 32))) (?v_34 ((_ sign_extend 8) T1_11017))) (let ((?v_59 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_34)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_34)) (_ bv8 32))) (_ bv65503 32))) (?v_33 ((_ sign_extend 8) T1_11018))) (let ((?v_58 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_33)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_33)) (_ bv8 32))) (_ bv65503 32))) (?v_25 ((_ sign_extend 8) T1_11019))) (let ((?v_57 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_25)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_25)) (_ bv8 32))) (_ bv65503 32))) (?v_19 ((_ sign_extend 8) T1_11020))) (let ((?v_21 (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_19)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_19)) (_ bv8 32))))) (let ((?v_56 (bvand ?v_21 (_ bv65503 32))) (?v_32 ((_ sign_extend 8) T1_11021))) (let ((?v_55 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_32)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_32)) (_ bv8 32))) (_ bv65503 32))) (?v_31 ((_ sign_extend 8) T1_11022))) (let ((?v_54 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_31)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_31)) (_ bv8 32))) (_ bv65503 32))) (?v_30 ((_ sign_extend 8) T1_11023))) (let ((?v_53 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_30)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_30)) (_ bv8 32))) (_ bv65503 32))) (?v_52 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_29)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_29)) (_ bv8 32))) (_ bv65503 32))) (?v_43 (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_28)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_28)) (_ bv8 32))))) (let ((?v_51 (bvand ?v_43 (_ bv65503 32))) (?v_27 ((_ sign_extend 8) T1_11026))) (let ((?v_50 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_27)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_27)) (_ bv8 32))) (_ bv65503 32))) (?v_49 (bvand (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_26)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_26)) (_ bv8 32))) (_ bv65503 32)))) (let ((?v_66 (bvadd ?v_49 (bvmul (bvadd ?v_50 (bvmul (bvadd ?v_51 (bvmul (bvadd ?v_52 (bvmul (bvadd ?v_53 (bvmul (bvadd ?v_54 (bvmul (bvadd ?v_55 (bvmul (bvadd ?v_56 (bvmul (bvadd ?v_57 (bvmul (bvadd ?v_58 (bvmul (bvadd ?v_59 (bvmul (bvadd ?v_60 (bvmul (bvadd ?v_61 (bvmul (bvadd ?v_62 (bvmul (bvadd ?v_63 (bvmul (bvadd ?v_64 (bvmul (bvadd ?v_65 (_ bv1515 32)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)))) (let ((?v_67 (bvor (bvashr (bvadd (bvmul ?v_66 (_ bv1103515245 32)) (_ bv12345 32)) ?v_41) (bvand (bvadd (bvmul ?v_66 (_ bv69069 32)) ?v_20) (_ bv4294901760 32)))) (?v_42 (bvadd ?v_49 (bvmul (bvadd ?v_50 (bvmul (bvadd ?v_51 (bvmul (bvadd ?v_52 (bvmul (bvadd ?v_53 (bvmul (bvadd ?v_54 (bvmul (bvadd ?v_55 (bvmul (bvadd ?v_56 (bvmul (bvadd ?v_57 (bvmul (bvadd ?v_58 (bvmul (bvadd ?v_59 (bvmul (bvadd ?v_60 (bvmul (bvadd ?v_61 (bvmul (bvadd ?v_62 (bvmul (bvadd ?v_63 (bvmul (bvadd ?v_64 (bvmul (bvadd ?v_65 (_ bv1031816 32)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)) ?v_2)))) (let ((?v_48 (bvor (bvashr (bvadd (bvmul ?v_42 (_ bv1103515245 32)) (_ bv12345 32)) ?v_41) (bvand (bvadd (bvmul ?v_42 (_ bv69069 32)) ?v_20) (_ bv4294901760 32)))) (?v_47 ((_ zero_extend 16) (_ bv25 16))) (?v_46 (bvsub ?v_43 (_ bv97 32))) (?v_45 (bvadd ?v_43 (_ bv65504 32))) (?v_44 ((_ zero_extend 24) (_ bv0 8))) (?v_23 (bvsub ?v_21 (_ bv97 32))) (?v_22 (bvadd ?v_21 (_ bv65504 32)))) (and true (not (= (bvand ?v_69 (_ bv0 32)) (_ bv0 32))) (not (= T1_11011 (_ bv0 8))) (bvult (_ bv25 32) (bvsub ?v_18 (_ bv97 32))) (= (bvadd (bvsub (_ bv0 32) ((_ zero_extend 24) (ite (not (= (bvadd ?v_21 (_ bv65426 32)) ?v_44)) (_ bv1 8) (_ bv0 8)))) ?v_20) (_ bv0 32)) (not (= (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_22)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_22)) (_ bv8 32))) ((_ zero_extend 16) (_ bv78 16)))) (bvule (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_23)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_23)) (_ bv8 32))) ?v_47) (bvult (_ bv25 32) (bvsub ?v_24 (_ bv97 32))) (not (= ?v_25 (_ bv0 16))) (= ?v_25 (_ bv47 16)) (not (= ?v_19 (_ bv78 16))) (not (= ?v_19 (_ bv0 16))) (not (= (bvadd (bvshl (bvand (bvand ?v_48 (_ bv7 32)) (_ bv7 32)) ?v_70) (_ bv146989572 32)) (_ bv0 32))) (= (bvadd (bvsub (_ bv0 32) ((_ zero_extend 24) (ite (not (= (bvadd ?v_43 (_ bv65422 32)) ?v_44)) (_ bv1 8) (_ bv0 8)))) ?v_20) (_ bv0 32)) (not (= (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_45)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_45)) (_ bv8 32))) ((_ zero_extend 16) (_ bv82 16)))) (bvule (bvadd ((_ zero_extend 24) ((_ extract 7 0) ?v_46)) (bvshl ((_ zero_extend 24) ((_ extract 15 8) ?v_46)) (_ bv8 32))) ?v_47) (= ?v_48 (_ bv3564909679 32)) (not (= ?v_48 (_ bv2600228911 32))) (= (_ bv112143823 32) ?v_67) (not (= ?v_67 (_ bv31678523 32))) (bvult (_ bv25 32) (bvsub ?v_68 (_ bv97 32))) (not (= ?v_29 (_ bv0 16))) (= ?v_29 (_ bv46 16)) (not (= ?v_28 (_ bv114 16))) (not (= (not (= ?v_26 (_ bv46 16))) (not true))) (not (= T1_11027 (_ bv92 8))) (not (= T1_11027 (_ bv47 8))) (not (= (bvadd (bvshl (bvand ?v_71 (_ bv7 32)) ?v_70) (_ bv146934788 32)) (_ bv0 32))) (bvule (_ bv0 32) ?v_71) (not (= ?v_69 (_ bv31678523 32)))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
